T:Type, P:(T), L2, L1:(T List). L1  L2  filter(P;L1)  filter(P;L2) 

latex

Definitions	t  T, Y, reduce(f;k;as), filter(P;l), x:A. B(x), P  Q, , ff, tt, if b then t else f fi , P & Q, P  Q, P  Q, Unit, ,
Lemmas	bool wf, iseg wf, assert of null, iseg nil, filter wf, nil iseg, ifthenelse wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, cons iseg, not wf, bnot wf, assert wf